Inference at * 1 1 1 0 2 1 
Iof proof for Lemma fincr formation:

.....wf..... NILNIL

1. P : 
2. j:. (k:. (k < j)  (P(k)))  (P(j))
3. n : 
  n+1   

latex

 by ArithMemberReflEqTypeCD 

latex

 1: 

 1:   n+1  
 2: .....set predicate..... NILNIL

 2:   0  (n+1)
 3: .....wf..... NILNIL

 3: 4. i : 
 3:   (0  i)  Type
 .

Definitions	Type, , s = t, #$n, n+m, f(a), a < b, P  Q, x:A. B(x), , x:AB(x), {x:A| B(x)} , A  B, , t  T
Lemmas	le wf